$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$ + top)), $e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (pred($e$) $\in$ $E$)